RCS "$Id: ModalityProtected.sig,v 1.3 1998/08/13 11:38:53 pxs Exp $";
(* This is the signature used by "friend" modules that need to know *)
(* more about modalities than we want to tell the whole world *)
signature MODALITY_PROTECTED =
  sig
    include MODALITY
    (* these functions are only here for the translation from big to   *)
    (* small logic   *)
    val justTau : modality
    val removeEps : modality -> modality
    val addTau : modality -> modality
    val positive : modality -> bool
    val mentionsEps : modality -> bool
    val le : modality * modality -> bool
    val eq : modality * modality -> bool
  end
